Nuprl Lemma : sends1-p_wf
11,40
postcript
pdf
x
,
tg
:Id,
k
:Knd,
l
:IdLnk,
T
,
A
,
B
:Type,
f
:(
A
B
(
T
List)),
es
:ES.
sends1-p(
es
;
x
;
A
;
k
;
B
;
l
;
tg
;
T
;
f
)
latex
Definitions
S
T
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
A
c
B
,
sends1-p(
es
;
x
;
A
;
k
;
B
;
l
;
tg
;
T
;
f
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
{
T
}
Lemmas
Id
wf
,
Knd
wf
,
IdLnk
wf
,
event
system
wf
,
es-vartype
wf
,
es-when
wf
,
es-val
wf
,
map
wf
,
es-locl
wf
,
l
before
wf
,
es-kind-rcv
,
es-sender
wf
,
iff
wf
origin
x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type, f:(A
B(T List)), es:ES.
x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type, f:(AB(T List)), es:ES.
T
Q
Q
x:A. B(x) Q
B Tx:A. B(x)